Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	admit(x,nil)	→ nil
2:	admit(x,u . (v . (w . z)))	→ cond(sum(x,u,v) = w,u . (v . (w . admit(carry(x,u,v),z))))
3:	cond(true,y)	→ y

There are 2 dependency pairs:


4:	ADMIT(x,u . (v . (w . z)))	→ COND(sum(x,u,v) = w,u . (v . (w . admit(carry(x,u,v),z))))
5:	ADMIT(x,u . (v . (w . z)))	→ ADMIT(carry(x,u,v),z)

The approximated dependency graph contains one SCC: {5}.

Consider the SCC {5}. There are no usable rules. By taking the AF π with π(ADMIT) = 2 and π(.) = [2] together with the lexicographic path order with empty precedence, rule 5 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.02 seconds) --- May 4, 2006